#pragma once
#include "Term.h"




class TermVariable : public Term
{

public:
	bool isTermVariable() const{return true;};
	virtual bool isFreeTermVariable() const = 0;
	virtual bool isBoundedTermVariable() const = 0;

public:
	TermVariable(const Type&, const string& ="");
	TermVariable(const TermVariable&);
	virtual ~TermVariable();

public:
		Term::pointer normalized() const;
		Token::pointer applyArgument(Token::const_reference)  const;
		bool isReducible() const{return false;};	   
};

class FreeTermVariable : public TermVariable{
public:
	bool isFreeTermVariable() const {return true;};
	bool isBoundedTermVariable() const {return false;};

public:
	FreeTermVariable(const Type&, const string& ="");

public:
		Token::pointer clone() const;
		bool TypeOccursinFreeVariable(Type::const_reference) const;
	};
class BoundedTermVariable : public TermVariable{	 
 public:
	bool isFreeTermVariable() const {return false;};
	bool isBoundedTermVariable() const {return true;};

public:
	BoundedTermVariable(const Type&);

public:
		Token::pointer clone() const;
		bool TypeOccursinFreeVariable(Type::const_reference Ty) const {return false;};
	};


